r:RngSig, u:|r|. r-Prime(u)   

latex

Up	rings 1
Definitions of Statement	r-Prime(u)
Definitions	P  Q, x f y, P  Q, P & Q, r-Prime(u), , t  T, x:A. B(x)
Lemmas	rng sig wf, rng times wf, rng car wf, rng one wf, ring divs wf, not wf